$\vdash$  $\mathbb{N}^{+}$ $\in$ Type